Nuprl Lemma : w-Msg_wf
11,40
postcript
pdf
the_w
:World. Msg
Type
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
Msg
,
w
.M
,
t
.1
,
t
.2
,
World
Lemmas
Msg
wf
,
world
wf
origin
the_w:World. Msg 
Type the_w:World. Msg Type x:A. B(x) T